2017

Clocked Lambda Calculus
Jörg Endrullis, Dimitri Hendriks, Jan Willem Klop, and Andrew Polonsky
Mathematical Structures in Computer Science , 27 (5) , pp. 782–806 (2017)
summary paper bib doi

Summary

We introduce the clocked lambda calculus, an extension of the classical lambda calculus with a unary symbol \( \tau \) that serves as a witness of \( \beta \)-steps. This calculus consists of the following two rules: \[ \begin{aligned} (\lambda x.M) N &\to \tau( M[x = N] ) \\ \tau(M)N &\to \tau(MN) \end{aligned} \] The clocked lambda-calculus is infinitary strongly normalizing, infinitary confluent, and the unique infinitary normal forms constitute enriched Böhm trees (more precisely, Lévy-Longo trees), which we call clocked Böhm trees. We show that clocked Böhm trees are suitable for discriminating a rich class of lambda terms having the same Böhm trees.

See research for an overview of my research on the clocked lambda claculus and fixed-point combinators.
Bibtex
```
@article{clocked:lambda:calculus:2017,
  author = {Endrullis, J\"{o}rg and Hendriks, Dimitri and Klop, Jan Willem and Polonsky, Andrew},
  title = {{Clocked Lambda Calculus}},
  journal = {Mathematical Structures in Computer Science},
  volume = {27},
  number = {5},
  pages = {782--806},
  year = {2017},
  doi = {10.1017/S0960129515000389},
  keywords = {rewriting, infinitary rewriting, lambda calculus},
  type = {journal}
}
```
Digital Object Identifier
```
10.1017/S0960129515000389
```

2014

Discriminating Lambda-Terms Using Clocked Boehm Trees
Jörg Endrullis, Dimitri Hendriks, Jan Willem Klop, and Andrew Polonsky
Logical Methods in Computer Science , 10 (2) (2014)
summary paper bib doi
Summary

As observed by Intrigila, there are hardly techniques available in the lambda calculus to prove that two lambda terms are not \( \beta \)-convertible. Techniques employing the usual Böhm trees are inadequate when we deal with terms having the same Böhm tree. This is the case in particular for fixed-point combinators, as they all have the same Böhm tree.

Another interesting equation, whose consideration was suggested by Scott, is BY = BYS, an equation valid in the classical model \( P \omega \) of lambda calculus, and hence valid with respect to Böhm tree-equality, but nevertheless the terms are \( \beta \)-inconvertible.

To prove such beta-inconvertibilities, we refine the concept of Böhm trees: we introduce clocked Böhm trees's with annotations that convey information of the tempo in which the Böhm trees are produced. Böhm trees are thus enriched with an intrinsic clock behaviour, leading to a refined discrimination method for lambda terms. An analogous approach pertains to Levy-Longo trees and Berarducci trees.

We illustrate applicability of our refined Böhm trees at the following examples:
- We show how to \( \beta \)-discriminate a large number of fixed-point combinators.
- We answer a question of Gordon Plotkin: Is there a fixed point combinator \( Y \) such that \[ Y ( \lambda z. f zz ) =_\beta Y ( \lambda x. Y ( \lambda y. f xy )) \]
We further increase the discrimination power of the technique by enhancing the precision of the clock, arriving at a notion that we call atomic clocks.

This paper is an extended version of Modular Construction of Fixed Point Combinators and Clocked Böhm Trees (LICS 2010).

See research for an overview of my research on the clocked lambda claculus and fixed-point combinators.
Bibtex
```
@article{lambda:clocks:2014,
  author = {Endrullis, J\"{o}rg and Hendriks, Dimitri and Klop, Jan Willem and Polonsky, Andrew},
  title = {{Discriminating Lambda-Terms Using Clocked Boehm Trees}},
  journal = {Logical Methods in Computer Science},
  volume = {10},
  number = {2},
  year = {2014},
  doi = {10.2168/LMCS-10(2:4)2014},
  keywords = {rewriting, infinitary rewriting, lambda calculus},
  type = {journal}
}
```
Digital Object Identifier
```
10.2168/LMCS-10(2:4)2014
```

Infinitary Term Rewriting for Weakly Orthogonal Systems: Properties and Counterexamples

Jörg Endrullis, Clemens Grabmayer, Dimitri Hendriks, Jan Willem Klop, and Vincent van Oostrom

Logical Methods in Computer Science , 10 (2:7) , pp. 1–33 (2014)

paper bib doi

Bibtex

@article{infinitary:weakly:orthogonal:2014,
  author = {Endrullis, J\"{o}rg and Grabmayer, Clemens and Hendriks, Dimitri and Klop, Jan Willem and van~Oostrom, Vincent},
  title = {{Infinitary Term Rewriting for Weakly Orthogonal Systems: Properties and Counterexamples}},
  journal = {Logical Methods in Computer Science},
  volume = {10},
  number = {2:7},
  pages = {1--33},
  year = {2014},
  doi = {10.2168/LMCS-10(2:7)2014},
  keywords = {rewriting, infinitary rewriting, lambda calculus},
  type = {journal}
}

Digital Object Identifier

10.2168/LMCS-10(2:7)2014

2013

Clocks for Functional Programs
Jörg Endrullis, Dimitri Hendriks, Jan Willem Klop, and Andrew Polonsky
In: The Beauty of Functional Code - Essays Dedicated to Rinus Plasmeijer on the Occasion of His 61st Birthday, pp. 97–126, Springer (2013)
summary paper bib doi

Summary

The contribution of this paper is twofold.

First, we derive a complete characterization of all simply-typed fixed-point combinator (fpc) generators using Barendregt's Inhabitation Machines. A fpc generator is a lambda term \( G \) such that \( Y G \) is a fpc whenever \( Y \) is. The term \( \delta = \lambda xy. y(xy) \), also known as Smullyan's Owl, is a famous fpc generator. For instance, Turing's fpc \( Y_1 \) can be obtaind from Curry's fpc \( Y_0 \) by postfixing \( \delta \): \[ Y_1 = Y_0 \delta \]

Second, we present a conjecture that vastly generalises Richard Statman's question on the existance of double fixed-point combinators. Statman asked whether there is a fixed-point combinator \( Y \) such that \( Y =_\beta Y \delta \). This question remains open as the proof by Benedetto Intrigila contains a gap. We have the following conjecture about the relation of the \( \mu \)-opertator and fixed-point combinators:

Conjecture

We conjecture that for any fixed-point combinator \( Y \) and simply-typed \( \lambda\mu \)-terms \( s,t \) it holds that \[ s =_{ \beta \mu } t \iff s_Y =_{ \beta } t_Y \] where \(s_Y, t_Y\) are the untyped lambda terms obtained from \(s,t\), respectively, by replacing all occurrences of \( \mu \)-operators with the fixed-point combinator \( Y \).

This conjecture immediately implies a negative answer to Statman's question.

See research for an overview of my research on the clocked lambda claculus and fixed-point combinators.
Bibtex
```
@inproceedings{lambda:clocks:functional:programs:2013,
  author = {Endrullis, J\"{o}rg and Hendriks, Dimitri and Klop, Jan Willem and Polonsky, Andrew},
  title = {{Clocks for Functional Programs}},
  booktitle = {The Beauty of Functional Code - Essays Dedicated to Rinus Plasmeijer on the Occasion of His 61st Birthday},
  pages = {97--126},
  year = {2013},
  doi = {10.1007/978-3-642-40355-2\_8},
  series = {LNCS},
  volume = {8106},
  publisher = {Springer},
  keywords = {rewriting, infinitary rewriting, lambda calculus},
  type = {journal}
}
```
Digital Object Identifier
```
10.1007/978-3-642-40355-2_8
```

2012

Highlights in Infinitary Rewriting and Lambda Calculus

Jörg Endrullis, Dimitri Hendriks, and Jan Willem Klop

Theoretical Computer Science , 464 , pp. 48–71 (2012)

paper bib doi

Bibtex

@article{infinitary:highlights:2012,
  author = {Endrullis, J\"{o}rg and Hendriks, Dimitri and Klop, Jan Willem},
  title = {{Highlights in Infinitary Rewriting and Lambda Calculus}},
  journal = {Theoretical Computer Science},
  volume = {464},
  pages = {48--71},
  year = {2012},
  doi = {10.1016/j.tcs.2012.08.018},
  keywords = {rewriting, infinitary rewriting, lambda calculus},
  type = {journal}
}

Digital Object Identifier

10.1016/j.tcs.2012.08.018

2010

Modular Construction of Fixed Point Combinators and Clocked Böhm Trees
Jörg Endrullis, Dimitri Hendriks, and Jan Willem Klop
In: Proc. Symp. on Logic in Computer Science (LICS 2010), pp. 111–119, IEEE Computer Society (2010)
summary paper bib doi

Summary

One of the best-known methods for discriminating lambda terms with respect to \( \beta \)-convertibility is due to Corrado Böhm. Roughly speaking, the Böhm tree of a lambda term is its infinite normal form. If lambda terms have distinct Böhm trees, then they are not \( \beta \)-convertible. But what if their Böhm trees coincide? For example, all fixed-point combinators have the same Böhm tree, namely \[ \lambda x. x(x(x(\ldots))) \]

We refine Böhm trees with a clock that records how many head reduction steps have been used to rewrite each subterm to head normal form. We show that clocked Böhm trees are suitable for discriminating a rich class of lambda terms (in particular many fixed-point combinators) having the same Böhm trees.

We refer to Discriminating Lambda-Terms Using Clocked Boehm Trees (LMCS 2014) for an extended journal version of this paper. In the extended version we improve the precision of the clocks to atomic clocks and we answer a question of Gordon Plotkin, showing that the method can be used beyond simple terms.

See research for an overview of my research on the clocked lambda claculus and fixed-point combinators.
Bibtex
```
@inproceedings{lambda:clocks:2010,
  author = {Endrullis, J\"{o}rg and Hendriks, Dimitri and Klop, Jan Willem},
  title = {{Modular Construction of Fixed Point Combinators and Clocked B\"{o}hm Trees}},
  booktitle = {Proc.\ Symp.\ on Logic in Computer Science (LICS~2010)},
  pages = {111--119},
  publisher = {{IEEE} Computer Society},
  year = {2010},
  doi = {10.1109/LICS.2010.8},
  keywords = {rewriting, infinitary rewriting, lambda calculus},
  type = {conference}
}
```
Digital Object Identifier
```
10.1109/LICS.2010.8
```

Unique Normal Forms in Infinitary Weakly Orthogonal Rewriting

Jörg Endrullis, Clemens Grabmayer, Dimitri Hendriks, Jan Willem Klop, and Vincent van Oostrom

In: Proc. Conf. on Rewriting Techniques and Applications (RTA 2010), pp. 85–102, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2010)

paper bib doi

Bibtex

@inproceedings{infinitary:weakly:orthogonal:unique:normal:forms:2010,
  author = {Endrullis, J\"{o}rg and Grabmayer, Clemens and Hendriks, Dimitri and Klop, Jan Willem and van~Oostrom, Vincent},
  title = {{Unique Normal Forms in Infinitary Weakly Orthogonal Rewriting}},
  booktitle = {Proc.\ Conf.\ on Rewriting Techniques and Applications (RTA~2010)},
  volume = {6},
  pages = {85--102},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
  series = {LIPIcs},
  year = {2010},
  doi = {10.4230/LIPIcs.RTA.2010.85},
  keywords = {rewriting, infinitary rewriting, lambda calculus},
  type = {conference}
}

Digital Object Identifier

10.4230/LIPIcs.RTA.2010.85

2008

Reduction under Substitution

Jörg Endrullis, and Roel C. de Vrijer

In: Proc. Conf. on Rewriting Techniques and Applications (RTA 2008), pp. 425–440, Springer (2008)

paper bib doi

Bibtex

@inproceedings{lambda:reduction:under:substitution:2008,
  author = {Endrullis, J\"{o}rg and de~Vrijer, Roel C.},
  title = {{Reduction under Substitution}},
  booktitle = {Proc.\ Conf.\ on Rewriting Techniques and Applications (RTA~2008)},
  volume = {5117},
  pages = {425--440},
  publisher = {Springer},
  series = {LNCS},
  year = {2008},
  doi = {10.1007/978-3-540-70590-1\_29},
  keywords = {rewriting, lambda calculus},
  type = {conference}
}

Digital Object Identifier

10.1007/978-3-540-70590-1_29

2017

Summary

Bibtex

Digital Object Identifier

2014

Summary

Bibtex

Digital Object Identifier

Bibtex

Digital Object Identifier

2013

Summary

Bibtex

Digital Object Identifier

2012

Bibtex

Digital Object Identifier

2010

Summary

Bibtex

Digital Object Identifier

Bibtex

Digital Object Identifier

2008

Bibtex

Digital Object Identifier